Mecanizaci��n de sem��ntica de lenguajes de programaci��n: teor��a, implementaci��n y desarrollo.

El presente proyecto se enmarca en el ��rea de m��todos formales para computaci��n; el objetivo de los m��todos formales es asegurar, a trav��s de herramientas l��gicas y matem��ticas, que sistemas computacionales satisfacen ciertas propiedades. El campo de sem��ntica de lenguajes de programaci��n trata justamente de construir modelos matemáticos que den cuenta de las diferentes caracter��sticas de cada lenguaje (estado mutable, mecanismos de paso de par��metros, ��rdenes de ejecuci��n, etc.); permitiendo razonar de una manera abstracta, en vez de lidiar con las peculiaridades de implementaciones o las vaguezas de descripciones informales. Como las pruebas formales de correcci��n son demasiado intrincadas, es muy conveniente realizar estos desarrollos te��ricos con la ayuda de asistentes de prueba. Este proceso de formalizar y corrobar aspectos sem��nticos a trav��s de un asistente se denomina mecanizaci��n de sem��ntica. Este proyecto ��� articulado en tres l��neas: sem��ntica de teor��a de tipos, implementaci��n de un lenguaje con tipos dependientes y sem��ntica de lenguajes imperativos con alto orden - se propone realizar avances en el estudio sem��ntico de lenguajes de programaci��n, mecanizar dichos resultados, e implementar un lenguaje con tipos dependientes con la intenci��n de que se convierta, en un mediano plazo, en un asistente de pruebas. En la l��nea de sem��ntica de teor��a de tipos los objetivos son: (a) extender el m��todo de normalizaci��n por evaluaci��n para construcciones no contempladas aun en la literatura, (b) probar la adecuaci��n de la implementaci��n en Haskell de dicho m��todo de normalizaci��n, y (c) construir nuevos modelos categ��ricos de teor��a de tipos. El objetivo de la segunda l��nea es el dise��o e implementaci��n de un lenguaje con tipos dependientes con la intenci��n de que el mismo se convierta en un asistente de pruebas. Una novedad de esta implementaci��n es que el algoritmo de chequeo de tipos es correcto y completo respecto al sistema formal, gracias a resultados ya obtenidos; adem��s la implementaci��n en Haskell del algoritmo de normalizaci��n (fundamental para el type-checking) tambi��n tendr�� su prueba de correcci��n. El foco de la tercera l��nea est�� en el estudio de lenguajes de programaci��n que combinan aspectos imperativos (estado mutable) con caracter��sticas de lenguajes funcionales (procedimientos y funciones). Por un lado se avanzar�� en la mecanizaci��n de pruebas de correcci��n de compiladores para lenguajes Algollike. El segundo aspecto de esta l��nea ser�� la definici��n de sem��nticas operacional y denotacional del lenguaje de programaci��n Lua y la posterior caracterizaci��n del mismo a partir de ellas. Para lograr dichos objetivos hemos dividido las tareas en actividades con metas graduales y que constituyen en s�� mismas aportes al estado del arte de cada una de las l��neas. La importancia acad��mica de este proyecto radica en los avances te��ricos que se propone en la l��nea de sem��ntica de teor��a de tipos, en las contribuci��n para la construcci��n de pruebas mecanizadas de correcci��n de compiladores, en el aporte que constituye la definici��n de una sem��ntica formal para el lenguaje Lua, y en el desarrollo de un lenguaje con tipos dependientes cuyos algoritmos m��s importantes est��n respaldados por pruebas de correcci��n. Adem��s, a nivel local, este proyecto permitir�� incorporar cuatro integrantes al grupo de ���Sem��ntica de la programaci��n���.